Nuprl Lemma : l_exists_append
11,40
postcript
pdf
T
:Type,
P
:(
T
),
L1
,
L2
:(
T
List). (
x
L1
@
L2
.
P
(
x
))
((
x
L1
.
P
(
x
))
(
x
L2
.
P
(
x
)))
latex
Definitions
x
.
t
(
x
)
,
{
T
}
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
(
x
L
.
P
(
x
))
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
A
c
B
,
True
Lemmas
member
append
,
and
functionality
wrt
iff
,
exists
functionality
wrt
iff
,
append
wf
,
l
member
wf
origin
T:Type, P:(T
), L1, L2:(T List). (
x
L1 @ L2.P(x)) 
((xL1.P(x)) 
(xL2.P(x))) T:Type, P:(T), L1, L2:(T List). (xL1 @ L2.P(x)) ((xL1.P(x)) (xL2.P(x))) 
x. t(x) T Q Qx:A. B(x) QxL.P(x)) Qx:A. B(x)
B